es:event_system{i:l}, d,b,a:es-E(es).
es-le(es; a; b)  es-le(es; a; d)  (||[a, b]|| = ||[a, d]||  )  (b = d) 

latex

Definitions	t  T, x:A. B(x), es-E(es), prop{i:l}, [e, e'], ||as||, P  Q, es-le(es; e; e'), es-locl(es; e; e'), guard(T), x. t(x), wellfounded{i:l}(A; x,y.R(x;y)), event_system{i:l}, A c B, P  Q, P  Q, P  Q, t.1, es-pred(es; e), P  Q, True, T, top, subtype(S; T), False, A, A  B, ge(i; j), (x  l)
Lemmas	le wf, member-es-interval, es-le-self, l member non nil, pos length, es-interval-eq, es-pred-one-one, length-append, top wf, squash wf, true wf, es-interval-less, es-le-pred, es-pred-locl, es-pred wf, es-le-iff, event system wf, es-locl-wellfnd, es-locl wf, es-le wf, length wf1, es-interval wf, es-E wf